M. Kikuchi, T. Kurahashi; "Liar-type paradoxes and the incompleteness phenomena"
著者
pdf
Abstract
We define a liar-type paradox as a consistent proposition in propositional modal logic which is obtained by attaching boxes to several subformulas of an inconsistent proposition in classical propositional logic, and show several famous paradoxes are liar-type. Then we show that we can generate a liar-type paradox from any inconsistent proposition in classical propositional logic and that undecidable sentences in arithmetic can be obtained from the existence of a liar-type paradox. We extend these results to predicate logic and discuss Yablo’s Paradox in this framework. Furthermore, we define explicit and implicit self-reference in paradoxes in the incompleteness phenomena.
メモ
様相論理の命題集合から算術の文に移す写像$ f \colon \mathrm{Prop}_\mathrm{M} \to \mathrm{Sent}_\mathrm{A}を実現(証明可能性論理)という. $ fを拡張して,様相論理の$ \Boxを理論$ Tの証明可能性述語として解釈するための写像$ f_T \colon \mathrm{Fml}_\mathrm{M} \mapsto \mathrm{Sent}_\mathrm{A}とする. すなわち,$ f_T(\Box A) \mapsto \mathrm{Pr}_T(\ulcorner f_T(A) \urcorner)とする.
Def:
$ \mathrm{M}(A) \coloneqq \{ B \mid \Box B \in \mathrm{Sub}(A) \}
$ \mathrm{H}(A) \coloneqq \bigwedge \{\Box B \to B \mid B \in \mathrm{M}(A)\}
Remark:
Kripkeモデル$ \mathcal{M} \coloneqq \lang W,\prec;\Vdash \rangには根$ r \in Wが存在することを要請する. 任意の$ x \in W \setminus \{r\}に対し$ r \prec x
命題様相論理の論理式$ Aに対して
Kripkeモデル$ \lang W,\prec;\Vdash \rangが$ A健全$ \iff根$ r \in Wで$ r \Vdash \mathrm{H}(A) Thm 1:
任意の命題様相論理の論理式$ Aに対して
任意のKripkeモデルの根$ rで$ r \Vdash A$ \iff$ \mathsf{GL} \vdash A 任意の$ A健全なKripkeモデルの根$ rで$ r \Vdash A$ \iff$ \mathsf{GLS} \vdash A proof
任意の実現$ fで$ T \vdash f_T(A)$ \iff$ \mathsf{GL} \vdash A
任意の実現$ fで$ \mathfrak{N} \vDash f_T(A)$ \iff$ \mathsf{GLS} \vdash A
Def: $ \Box簡約
様相命題論理の論理式$ Aに対して$ A^*を$ Aの$ \Box簡約という. 1. $ p^* \mapsto p
2. $ (\lnot A)^* \mapsto \lnot A^*
3. $ (A \circ B)^* \mapsto A^* \circ B^*
$ \circ = \lor,\land,\to,\leftrightarrow
4. $ (\Box A)^* \mapsto A^*
remark:
任意の$ A^*は命題論理の論理式である.すなわち$ \circ^* \colon \mathrm{Fml}_\mathrm{M} \mapsto \mathrm{Fml}_\mathrm{PL} Def: $ \sf GL無矛盾 / $ \sf GLS無矛盾
$ Aが$ \sf GL無矛盾$ \iff$ \sf GL \nvdash \lnot A
$ Aが$ \sf GLS無矛盾$ \iff$ \sf GLS \nvdash \lnot A
$ Aが$ \sf GL嘘つき型パラドックス論理式Liar-type Paradox
$ \iff$ Aが$ \sf GL無矛盾かつ,$ A^*が命題論理の上で矛盾する.
$ Aが$ \sf GL厳密嘘つき型パラドクス論理式Strict Liar-type Paradox
$ \iff$ Aが$ \sf GL嘘つき型パラドクス論理式かつ,$ \mathrm{M}(A)が命題変項しか含まない.
remark:
remark:
$ fを実現,$ \mathfrak{M}を$ Tのモデルとする.
$ \iff$ \mathfrak{M} \vDash f_T(A)かつ$ A^*が命題論理上で矛盾する
$ \iff$ Aが$ \mathfrak{M}内$ f上嘘つき型パラドックス論理式かつ,$ \mathrm{M}(A)が命題変項しか含まない. Prop 1:
Remark:
$ A \equiv p \leftrightarrow \lnot \Box pとする.
1. このとき,$ \mathrm{M}(A) = \{p\}
2. $ A^* \equiv p \leftrightarrow \lnot pより明らかに命題論理で矛盾
$ Gは$ TのGödel文とし,$ f_T(p) \mapsto Gとなる$ fを取ってくる. このとき$ f_T(A) \mapsto G \leftrightarrow \lnot \mathrm{Pr}_T(\ulcorner G \urcorner)
3. $ \sf PAが健全だとすると,$ \mathfrak{N} \vDash f_T(A)
$ p_1,\dots,p_5.$ p_iは「$ i日目にテストを行う」を意味する
$ \Box p_iは「生徒が$ i日目にテストを行うことを知っている」を意味する.
$ \Box p_i \to \lnot p_iは抜き打ち性「テストの日付を知られたらテストをしない」を表す.
$ \bigvee_{1 \leq i \leq 5} p_i \land \bigwedge_{1 \leq i < j \leq 5}\lnot(p_i \land p_j)は「どこかの日でテストを行い,それ以外の日ではテストを行わない」ことを意味する.
これらをつなげる.
$ A \equiv \bigvee_{1 \leq i \leq 5} p_i \land \bigwedge_{1 \leq i < j \leq 5}\lnot(p_i \land p_j) \land \bigwedge_{1 \leq i \leq 5}( \Box p_i \to \lnot p_i)
$ \mathrm{M}(A) = \{p_1,\dots,p_5\}
$ A^*は命題論理で矛盾する.
remark
ややこしいので2日で考える
$ A_2 \equiv (p_1 \lor p_2) \land \lnot(p_1 \land p_2) \land (\Box p_1 \to \lnot p_1) \land (\Box p_2 \to \lnot p_2)
$ A_2^* \equiv (p_1 \lor p_2) \land \lnot(p_1 \land p_2) \land (p_1 \to \lnot p_1) \land (p_2 \to \lnot p_2)
$ A_2^* \equiv (p_1 \lor p_2) \land (\lnot p_1 \lor \lnot p_2) \land \lnot p_1 \land \lnot p_2
以下を満たす$ fを取ってくる
$ TのGödel文を$ Gとして$ f_T(p_1) \mapsto G $ i = 2,\dots,5に対して$ f_T(p_i) \mapsto 0 = 1
$ pは真だが,私は$ pが真だと信じない.
$ A \equiv p \land \lnot \Box pと形式化すれば,Example1と同じ様に.
この文が証明できると仮定すれば,$ Bは正しい.
$ A \equiv p \leftrightarrow (\Box p \to B)
ただし$ Bは$ pを含まない論理式とする.
$ A^* \equiv p \leftrightarrow (p \to B^*)より,$ A^*が矛盾$ \iff$ B^*が矛盾
$ TのKreisel文$ Kとなるような,すなわち$ \mathsf{PA} \vdash K \leftrightarrow (\mathrm{Pr}_T(\ulcorner K \urcorner) \to f_T(B))となるような$ fを取る. $ g(p) \mapsto Kかつ$ q \neq pな$ qに対し$ g(q) \mapsto f(q)となるような$ gを取る.
このとき,$ Bは$ pを含まないので$ g_T(B) \mapsto f_T(B).
$ \mathsf{PA} \vdash g_T(A).
$ g_T(A) \mapsto K \leftrightarrow (\mathrm{Pr}_T(\ulcorner K \urcorner) \to f_T(B))
$ \sf PAの健全性より$ \mathfrak{N} \vDash g_T(A)
Example 5:
実際
$ \mathsf{GL} \nvdash \lnot Aであるので$ \sf GL無矛盾
他方,$ \mathsf{GLS} \vdash \lnot Aであるため$ \sf GLS無矛盾ではない.$ \lnot A \equiv \Box p \to pは$ \sf Sより即座に導かれる.
$ \sf GL,GLSの拡張を$ \sf QGL,QGLSという.Quantifier
ただし演算子,定数,等号を含まない.
このとき実現は拡張される.
$ f(P(\vec{x})) \mapsto \varphi(\vec{x})
$ P(\vec{x})は様相述語論理上の述語
$ \varphi(\vec{x})は$ \mathscr{L}_\mathrm{A}の自由変数を$ \vec{x}とする論理式